(in category theory/type theory/computer science)
of all homotopy types
of (-1)-truncated types/h-propositions
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In a constructive weakly predicative structural set theory, such as doing mathematics in a well-pointed cartesian closed lextensive coherent category with a natural numbers object, it is still possible to define a category inside of the set theory, and in particular, it is still possible to define a well-pointed cartesian closed lextensive coherent category object with a natural numbers object inside of any well-pointed cartesian closed lextensive coherent category with a natural numbers object. These objects are called universes or Grothendieck universes in structural set theory. From here, one could form the sub-(0,1)-category of subterminal objects in , the set of -small subsingletons, and subsingletons model propositions in the universe, so could be called a set of -small propositions as well.
If a set theory has multiple such universes and , then there are multiple such sets of propositions, one of which is -small, and another one of which is -small. In general, the set of -small propositions and the set of -small propositions cannot be proven to be equivalent to each other. However, propositional resizing is the axiom that for universe and , the set of -small propositions is in bijection with the set of -small propositions, .
In homotopy type theory, the type of h-propositions of a Tarski universe (or Russell universe) is not in general essentially -small. Propositional resizing is then the statement that the type of h-propositions is essentially -small.
There is a separate axiom of propositional resizing for a hierarchy of universes, where the type of h-propositions of each universe, where one universe embeds into the other universe, are equivalent to each other.
Propositional resizing is a form of impredicativity for h-propositions, and by avoiding its use, the universe or hierarchy is said to remain predicative.
However, when using Tarski universes, while universes and universe hierarchies may be impredicative, the overarching type theory is still predicative if it has a judgment ‘’, since it is impossible to talk about all types.
We work in a structural set theory which externally forms a well-pointed cartesian closed lextensive coherent category with a natural numbers object, namely a structural set theory with
Any well-pointed cartesian closed coherent category with a natural numbers object inside of the set theory is thus an internal model of the set theory, and thus could be considered to be a universe inside of the set theory.
…
Let be a weakly Tarski universe and let
be the type of all propositions in . The weakly Tarski universe is impredicative or satisfies propositional resizing if it has a term and an equivalence
A weakly Tarski universe is strictly impredicative or satisfies strict propositional resizing if the above equivalence becomes a definitional equality:
In particular, every impredicative strictly Tarski universe is strictly impredicative.
Let be a hierarchy of weakly Tarski universes. By definition, is a preorder and there is a function
which states that for all terms and implies the type of embeddings is pointed. We thus have a natural map
which is the restriction of the above function to small propositions of the universe.
The axiom of proposition resizing states that for all terms , , and the embedding is an equivalence of types
The type of all h-propositions in the larger universe may be resized to be equivalent to the type of all h-proposition in the smaller universe . The universe hierarchy is then said to be impredicative.
Usually, the hierarchy of Tarski universes is a sequential hierarchy indexed by the natural numbers .
Last revised on October 15, 2022 at 12:30:10. See the history of this page for a list of all contributions to it.